\begin{tabbing}
R{-}da($R$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ 
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.fpf{-}join(KindDeq;${\it rec}_{1}$;${\it rec}_{2}$)
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ 
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ 
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ 
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ ${\it knd}$ : $T$ else  fi
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ \=if source($l$) = $i$$\rightarrow$ fpf{-}join(KindDeq;${\it knd}$ : $T$;lnk{-}decl($l$;${\it dt}$))\+
\\[0ex]else  fi
\-\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ locl($a$) : $T$ else  fi
\\[0ex]Raframe(${\it loc}$,$k$,$L$)=$>$ 
\\[0ex]Rbframe(${\it loc}$,$k$,$L$)=$>$ 
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ 
\-
\end{tabbing}